$\forall$$T$:Type, $R$, $Q$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$), $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]Trans($T$;$x$,$y$.$Q$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. ($Q$($x$,$y$)) $\Rightarrow$ ($\neg$($Q$($y$,$x$))))
\\[0ex]$\Rightarrow$ $R$ =$>$ $Q$
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. ($P$($x$) \& $P$($y$)) $\Rightarrow$ ((($R$($x$,$y$)) $\vee$ ($x$ = $y$)) $\vee$ ($R$($y$,$x$))))
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. ($P$($x$) \& $P$($y$)) $\Rightarrow$ (($R$($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($Q$($x$,$y$))))